$\forall$$T$:Type, $X$:MaInterface($T$). ma{-}interface{-}inl($X$) $\in$ MaInterface(\{$x$:$T$ + Top$\mid$ $\uparrow$isl($x$)\} )